|
|
Nástoj pro abstraktní regulární stromový model checking
Mráz, Patrik ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Formálna verifikácia sa zaoberá dokazovaním korektnosti systému podľa daných špecifikácií.Jej potrebu znásobuje stále väčšia rozšírenosť počítačov a neustály rast zložitosti aj rozsiahlosti vyvíjaných systémov. Cieľom tejto práce je implementácia nástroja formálnejverifikácie abstraktný regulárny stromový model checking (ARTMC) nad knižnicou VATA. Pre dosiahnutie tohto cieľa bolo potrebné rozšíriť knižnicu VATA o konečné stromové prevodníky,abstrakcie stromových automatov a integrovať ich spolu s nástrojom ARTMC doknižnice VATA.
|
|
|
Překladač z fragmentu jazyka C do nástroje ARTMC
Marušák, Matej ; Hruška, Martin (oponent) ; Rogalewicz, Adam (vedoucí práce)
S narastajúcou komplexitou softvérových programov je stále viac a viac žiadaná automa- tizovaná analýza a verifikácia týchto programov. Výskumná skupina VeriFIT na Fakulte informačních technologií Vysokého učení technického sa zaoberá výskumom v danej oblasti. Jedným z vytvorených nástrojov v tejto skupine je aj nástroj ARTMC. Táto bakalárska práca navrhuje a implementuje prekladač z podmnožiny jazyka C do vstupného formátu ná- stroja ARTMC. Vytvorený prekladač výrazne uľahčuje prácu s nástrojom ARTMC, nakoľko vstupný formát nie je vhodný na manuálné vytváranie.
|
|
|
Překladač z fragmentu jazyka C do nástroje ARTMC
Marušák, Matej ; Hruška, Martin (oponent) ; Rogalewicz, Adam (vedoucí práce)
S narastajúcou komplexitou softvérových programov je stále viac a viac žiadaná automa- tizovaná analýza a verifikácia týchto programov. Výskumná skupina VeriFIT na Fakulte informačních technologií Vysokého učení technického sa zaoberá výskumom v danej oblasti. Jedným z vytvorených nástrojov v tejto skupine je aj nástroj ARTMC. Táto bakalárska práca navrhuje a implementuje prekladač z podmnožiny jazyka C do vstupného formátu ná- stroja ARTMC. Vytvorený prekladač výrazne uľahčuje prácu s nástrojom ARTMC, nakoľko vstupný formát nie je vhodný na manuálné vytváranie.
|
|
|
Nástoj pro abstraktní regulární stromový model checking
Mráz, Patrik ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Formálna verifikácia sa zaoberá dokazovaním korektnosti systému podľa daných špecifikácií.Jej potrebu znásobuje stále väčšia rozšírenosť počítačov a neustály rast zložitosti aj rozsiahlosti vyvíjaných systémov. Cieľom tejto práce je implementácia nástroja formálnejverifikácie abstraktný regulárny stromový model checking (ARTMC) nad knižnicou VATA. Pre dosiahnutie tohto cieľa bolo potrebné rozšíriť knižnicu VATA o konečné stromové prevodníky,abstrakcie stromových automatov a integrovať ich spolu s nástrojom ARTMC doknižnice VATA.
|
host ::
RSS.